COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	PROOFS OF NON-TERMINATION
C00005 ENDMK
C⊗;
PROOFS OF NON-TERMINATION


	If a procedure terminates for given arguments, this fact can be
proved by running the procedure until it stops.  Given any set of axioms
about procedures, there are some procedures that don't terminate and 
cannot be proved not to terminate from these axioms.  Indeed, given a
partial decision procedure for termination, one can generate from this
decision procedure, a procedure whose non¬termination, this procedure
does not show.  This is shown in my LISP notes - the October 1973 version
of which is ch4.2(206,jmc].

	Nevertheless, it is quite feasible to show that many procedures
don't terminate.  The simplest procedure that doesn't terminate
has the recursive definition

	loop(x) ← loop(x),

and others can be shown not to terminate by setting up a homomorphism between
the other procedure and this standard non terminator.

	It may be that given a sufficiently general notion of homomorphism,
any procedure that can be shown not to terminate, can be so shown by
a homomorphism with loop.

	In any case, methods for proving procedures non-terminating for
particular arguments have not been explored and may prove interesting.
Perhaps they are akin to showing that models exist for a collection of
sentences in predicate calculus, since proving theorems in predicate
calculus is just showing that a model does not exist for the negation of
the theorem, and proving termination is a special case of proving a 
theorem.  (Given time, I can be more convincing about the validity of
this analogy.  I can also tell more about homomorphisms between procedures).

	This is suggested as a thesis topic in MTC.